es:event_system{i:l}, e:es-E(es), x:Id, T:Type, v:T.
es-dtype(es; loc(e); x; T)
 (es-first(es; e))
 ((es-initially(es; loc(e); x) = v)  (es-when(es; x; e) = v)) 

latex

Definitions	x:AB(x), P  Q, t  T, x:A. B(x), loc(e), es-dtype(es; i; x; T), s = t, x:A  B(x), event_system{i:l}, t.1, es-E(es), atom{$n:n}, Id, Type, es-first(es; e), b, es-vartype(es; i; x), P  Q, es-when(es; x; e), if b then t else f fi , prop{i:l}, es-initially(es; i; x), <a, b>, P  Q, P  Q
Lemmas	es-discrete-when-first, event system wf, es-E wf, es-initially wf, es-when wf, es-vartype wf, subtype rel self, Id wf, assert wf, es-first wf, es-dtype wf, es-loc wf